r,s:rationals. (r + s)  rationals 

latex

Definitions	P  Q, P  Q, P  Q, prop{i:l}, guard(T), P  Q, sq_type(T), top, qeq(r; s), nequal(T; a; b), ff, if b then t else f fi , tt, int_nzero, b-union(A; B), r + s, t  T, rationals, x:A. B(x),
Lemmas	mul add distrib, assert of eq int, eq int wf, eqtt to assert, isint-int, nequal wf, mul nzero, bfalse wf, int nzero wf, ifthenelse wf, rationals wf, btrue wf, qeq wf, bool wf